0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 284 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 482 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 15 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 30 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPOrderProof (⇔, 232 ms)
↳43 QDP
↳44 DependencyGraphProof (⇔, 0 ms)
↳45 TRUE
↳46 PiDP
↳47 UsableRulesProof (⇔, 0 ms)
↳48 PiDP
↳49 PiDPToQDPProof (⇒, 0 ms)
↳50 QDP
↳51 QDPSizeChangeProof (⇔, 0 ms)
↳52 YES
↳53 PiDP
↳54 UsableRulesProof (⇔, 0 ms)
↳55 PiDP
↳56 PiDPToQDPProof (⇒, 0 ms)
↳57 QDP
↳58 QDPOrderProof (⇔, 146 ms)
↳59 QDP
↳60 DependencyGraphProof (⇔, 0 ms)
↳61 TRUE
QSORTF_IN_GA(.(X1, []), X2) → U21_GA(X1, X2, qsortcA_in_a(X3))
U21_GA(X1, X2, qsortcA_out_a(X3)) → U22_GA(X1, X2, X3, qsortcA_in_a(X4))
U22_GA(X1, X2, X3, qsortcA_out_a(X4)) → U23_GA(X1, X2, appendB_in_ggga(X3, X1, X4, X2))
U22_GA(X1, X2, X3, qsortcA_out_a(X4)) → APPENDB_IN_GGGA(X3, X1, X4, X2)
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U1_GGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X2, X3, X4, X5))
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U24_GA(X1, X2, X3, X4, leC_in_gg(X2, X1))
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → LEC_IN_GG(X2, X1)
LEC_IN_GG(s(X1), s(X2)) → U2_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U25_GA(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U26_GA(X1, X2, X3, X4, splitD_in_ggaa(X3, X1, X5, X6))
U25_GA(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → SPLITD_IN_GGAA(X3, X1, X5, X6)
SPLITD_IN_GGAA(.(X1, X2), X3, .(X1, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, leC_in_gg(X1, X3))
SPLITD_IN_GGAA(.(X1, X2), X3, .(X1, X4), X5) → LEC_IN_GG(X1, X3)
SPLITD_IN_GGAA(.(X1, X2), X3, .(X1, X4), X5) → U4_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U5_GGAA(X1, X2, X3, X4, X5, splitD_in_ggaa(X2, X3, X4, X5))
U4_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
SPLITD_IN_GGAA(.(X1, X2), X3, X4, .(X1, X5)) → U6_GGAA(X1, X2, X3, X4, X5, gtE_in_gg(X1, X3))
SPLITD_IN_GGAA(.(X1, X2), X3, X4, .(X1, X5)) → GTE_IN_GG(X1, X3)
GTE_IN_GG(s(X1), s(X2)) → U9_GG(X1, X2, gtE_in_gg(X1, X2))
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
SPLITD_IN_GGAA(.(X1, X2), X3, X4, .(X1, X5)) → U7_GGAA(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U8_GGAA(X1, X2, X3, X4, X5, splitD_in_ggaa(X2, X3, X4, X5))
U7_GGAA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
U25_GA(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U28_GA(X1, X2, X3, X4, qsortF_in_ga(.(X2, X5), X7))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSORTF_IN_GA(.(X2, X5), X7)
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U31_GA(X1, X2, X3, X4, gtE_in_gg(X2, X1))
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → GTE_IN_GG(X2, X1)
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U32_GA(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U32_GA(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U33_GA(X1, X2, X3, X4, splitD_in_ggaa(X3, X1, X5, X6))
U32_GA(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → SPLITD_IN_GGAA(X3, X1, X5, X6)
U32_GA(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U34_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U35_GA(X1, X2, X3, X4, qsortH_in_ga(X5, X7))
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSORTH_IN_GA(X5, X7)
QSORTH_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, splitD_in_ggaa(X2, X1, X4, X5))
QSORTH_IN_GA(.(X1, X2), X3) → SPLITD_IN_GGAA(X2, X1, X4, X5)
QSORTH_IN_GA(.(X1, X2), X3) → U11_GA(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U12_GA(X1, X2, X3, qsortH_in_ga(X4, X6))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → QSORTH_IN_GA(X4, X6)
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U13_GA(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U14_GA(X1, X2, X3, qsortH_in_ga(X5, X7))
U13_GA(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → QSORTH_IN_GA(X5, X7)
U13_GA(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U15_GA(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U15_GA(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U16_GA(X1, X2, X3, appendI_in_ggga(X6, X1, X7, X3))
U15_GA(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → APPENDI_IN_GGGA(X6, X1, X7, X3)
APPENDI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U17_GGGA(X1, X2, X3, X4, X5, appendI_in_ggga(X2, X3, X4, X5))
APPENDI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDI_IN_GGGA(X2, X3, X4, X5)
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U36_GA(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U36_GA(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U37_GA(X1, X2, X3, X4, pG_in_gagga(.(X2, X6), X8, X7, X1, X4))
U36_GA(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → PG_IN_GAGGA(.(X2, X6), X8, X7, X1, X4)
PG_IN_GAGGA(X1, X2, X3, X4, X5) → U18_GAGGA(X1, X2, X3, X4, X5, qsortH_in_ga(X1, X2))
PG_IN_GAGGA(X1, X2, X3, X4, X5) → QSORTH_IN_GA(X1, X2)
PG_IN_GAGGA(X1, X2, X3, X4, X5) → U19_GAGGA(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U19_GAGGA(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U20_GAGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X3, X4, X2, X5))
U19_GAGGA(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → APPENDB_IN_GGGA(X3, X4, X2, X5)
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U29_GA(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
U29_GA(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U30_GA(X1, X2, X3, X4, pG_in_gagga(X6, X8, X7, X1, X4))
U29_GA(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → PG_IN_GAGGA(X6, X8, X7, X1, X4)
qsortcA_in_a([]) → qsortcA_out_a([])
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
qsortcF_in_ga([], []) → qsortcF_out_ga([], [])
qsortcF_in_ga(.(X1, []), X2) → U46_ga(X1, X2, qsortcA_in_a(X3))
U46_ga(X1, X2, qsortcA_out_a(X3)) → U47_ga(X1, X2, X3, qsortcA_in_a(X4))
U47_ga(X1, X2, X3, qsortcA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qsortcF_out_ga(.(X1, []), X2)
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
QSORTF_IN_GA(.(X1, []), X2) → U21_GA(X1, X2, qsortcA_in_a(X3))
U21_GA(X1, X2, qsortcA_out_a(X3)) → U22_GA(X1, X2, X3, qsortcA_in_a(X4))
U22_GA(X1, X2, X3, qsortcA_out_a(X4)) → U23_GA(X1, X2, appendB_in_ggga(X3, X1, X4, X2))
U22_GA(X1, X2, X3, qsortcA_out_a(X4)) → APPENDB_IN_GGGA(X3, X1, X4, X2)
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U1_GGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X2, X3, X4, X5))
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U24_GA(X1, X2, X3, X4, leC_in_gg(X2, X1))
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → LEC_IN_GG(X2, X1)
LEC_IN_GG(s(X1), s(X2)) → U2_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U25_GA(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U26_GA(X1, X2, X3, X4, splitD_in_ggaa(X3, X1, X5, X6))
U25_GA(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → SPLITD_IN_GGAA(X3, X1, X5, X6)
SPLITD_IN_GGAA(.(X1, X2), X3, .(X1, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, leC_in_gg(X1, X3))
SPLITD_IN_GGAA(.(X1, X2), X3, .(X1, X4), X5) → LEC_IN_GG(X1, X3)
SPLITD_IN_GGAA(.(X1, X2), X3, .(X1, X4), X5) → U4_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U5_GGAA(X1, X2, X3, X4, X5, splitD_in_ggaa(X2, X3, X4, X5))
U4_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
SPLITD_IN_GGAA(.(X1, X2), X3, X4, .(X1, X5)) → U6_GGAA(X1, X2, X3, X4, X5, gtE_in_gg(X1, X3))
SPLITD_IN_GGAA(.(X1, X2), X3, X4, .(X1, X5)) → GTE_IN_GG(X1, X3)
GTE_IN_GG(s(X1), s(X2)) → U9_GG(X1, X2, gtE_in_gg(X1, X2))
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
SPLITD_IN_GGAA(.(X1, X2), X3, X4, .(X1, X5)) → U7_GGAA(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U8_GGAA(X1, X2, X3, X4, X5, splitD_in_ggaa(X2, X3, X4, X5))
U7_GGAA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
U25_GA(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U28_GA(X1, X2, X3, X4, qsortF_in_ga(.(X2, X5), X7))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSORTF_IN_GA(.(X2, X5), X7)
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U31_GA(X1, X2, X3, X4, gtE_in_gg(X2, X1))
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → GTE_IN_GG(X2, X1)
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U32_GA(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U32_GA(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U33_GA(X1, X2, X3, X4, splitD_in_ggaa(X3, X1, X5, X6))
U32_GA(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → SPLITD_IN_GGAA(X3, X1, X5, X6)
U32_GA(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U34_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U35_GA(X1, X2, X3, X4, qsortH_in_ga(X5, X7))
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSORTH_IN_GA(X5, X7)
QSORTH_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, splitD_in_ggaa(X2, X1, X4, X5))
QSORTH_IN_GA(.(X1, X2), X3) → SPLITD_IN_GGAA(X2, X1, X4, X5)
QSORTH_IN_GA(.(X1, X2), X3) → U11_GA(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U12_GA(X1, X2, X3, qsortH_in_ga(X4, X6))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → QSORTH_IN_GA(X4, X6)
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U13_GA(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U14_GA(X1, X2, X3, qsortH_in_ga(X5, X7))
U13_GA(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → QSORTH_IN_GA(X5, X7)
U13_GA(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U15_GA(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U15_GA(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U16_GA(X1, X2, X3, appendI_in_ggga(X6, X1, X7, X3))
U15_GA(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → APPENDI_IN_GGGA(X6, X1, X7, X3)
APPENDI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U17_GGGA(X1, X2, X3, X4, X5, appendI_in_ggga(X2, X3, X4, X5))
APPENDI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDI_IN_GGGA(X2, X3, X4, X5)
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U36_GA(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U36_GA(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U37_GA(X1, X2, X3, X4, pG_in_gagga(.(X2, X6), X8, X7, X1, X4))
U36_GA(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → PG_IN_GAGGA(.(X2, X6), X8, X7, X1, X4)
PG_IN_GAGGA(X1, X2, X3, X4, X5) → U18_GAGGA(X1, X2, X3, X4, X5, qsortH_in_ga(X1, X2))
PG_IN_GAGGA(X1, X2, X3, X4, X5) → QSORTH_IN_GA(X1, X2)
PG_IN_GAGGA(X1, X2, X3, X4, X5) → U19_GAGGA(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U19_GAGGA(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U20_GAGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X3, X4, X2, X5))
U19_GAGGA(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → APPENDB_IN_GGGA(X3, X4, X2, X5)
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U29_GA(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
U29_GA(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U30_GA(X1, X2, X3, X4, pG_in_gagga(X6, X8, X7, X1, X4))
U29_GA(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → PG_IN_GAGGA(X6, X8, X7, X1, X4)
qsortcA_in_a([]) → qsortcA_out_a([])
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
qsortcF_in_ga([], []) → qsortcF_out_ga([], [])
qsortcF_in_ga(.(X1, []), X2) → U46_ga(X1, X2, qsortcA_in_a(X3))
U46_ga(X1, X2, qsortcA_out_a(X3)) → U47_ga(X1, X2, X3, qsortcA_in_a(X4))
U47_ga(X1, X2, X3, qsortcA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qsortcF_out_ga(.(X1, []), X2)
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
APPENDI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDI_IN_GGGA(X2, X3, X4, X5)
qsortcA_in_a([]) → qsortcA_out_a([])
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
qsortcF_in_ga([], []) → qsortcF_out_ga([], [])
qsortcF_in_ga(.(X1, []), X2) → U46_ga(X1, X2, qsortcA_in_a(X3))
U46_ga(X1, X2, qsortcA_out_a(X3)) → U47_ga(X1, X2, X3, qsortcA_in_a(X4))
U47_ga(X1, X2, X3, qsortcA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qsortcF_out_ga(.(X1, []), X2)
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
APPENDI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDI_IN_GGGA(X2, X3, X4, X5)
APPENDI_IN_GGGA(.(X1, X2), X3, X4) → APPENDI_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
qsortcA_in_a([]) → qsortcA_out_a([])
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
qsortcF_in_ga([], []) → qsortcF_out_ga([], [])
qsortcF_in_ga(.(X1, []), X2) → U46_ga(X1, X2, qsortcA_in_a(X3))
U46_ga(X1, X2, qsortcA_out_a(X3)) → U47_ga(X1, X2, X3, qsortcA_in_a(X4))
U47_ga(X1, X2, X3, qsortcA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qsortcF_out_ga(.(X1, []), X2)
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
qsortcA_in_a([]) → qsortcA_out_a([])
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
qsortcF_in_ga([], []) → qsortcF_out_ga([], [])
qsortcF_in_ga(.(X1, []), X2) → U46_ga(X1, X2, qsortcA_in_a(X3))
U46_ga(X1, X2, qsortcA_out_a(X3)) → U47_ga(X1, X2, X3, qsortcA_in_a(X4))
U47_ga(X1, X2, X3, qsortcA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qsortcF_out_ga(.(X1, []), X2)
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
SPLITD_IN_GGAA(.(X1, X2), X3, .(X1, X4), X5) → U4_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
SPLITD_IN_GGAA(.(X1, X2), X3, X4, .(X1, X5)) → U7_GGAA(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
qsortcA_in_a([]) → qsortcA_out_a([])
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
qsortcF_in_ga([], []) → qsortcF_out_ga([], [])
qsortcF_in_ga(.(X1, []), X2) → U46_ga(X1, X2, qsortcA_in_a(X3))
U46_ga(X1, X2, qsortcA_out_a(X3)) → U47_ga(X1, X2, X3, qsortcA_in_a(X4))
U47_ga(X1, X2, X3, qsortcA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qsortcF_out_ga(.(X1, []), X2)
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
SPLITD_IN_GGAA(.(X1, X2), X3, .(X1, X4), X5) → U4_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
SPLITD_IN_GGAA(.(X1, X2), X3, X4, .(X1, X5)) → U7_GGAA(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
SPLITD_IN_GGAA(.(X1, X2), X3) → U4_GGAA(X1, X2, X3, lecC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, lecC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3)
SPLITD_IN_GGAA(.(X1, X2), X3) → U7_GGAA(X1, X2, X3, gtcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, gtcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3)
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
lecC_in_gg(x0, x1)
gtcE_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U45_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
QSORTH_IN_GA(.(X1, X2), X3) → U11_GA(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → QSORTH_IN_GA(X4, X6)
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U13_GA(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → QSORTH_IN_GA(X5, X7)
qsortcA_in_a([]) → qsortcA_out_a([])
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
qsortcF_in_ga([], []) → qsortcF_out_ga([], [])
qsortcF_in_ga(.(X1, []), X2) → U46_ga(X1, X2, qsortcA_in_a(X3))
U46_ga(X1, X2, qsortcA_out_a(X3)) → U47_ga(X1, X2, X3, qsortcA_in_a(X4))
U47_ga(X1, X2, X3, qsortcA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qsortcF_out_ga(.(X1, []), X2)
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
QSORTH_IN_GA(.(X1, X2), X3) → U11_GA(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → QSORTH_IN_GA(X4, X6)
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U13_GA(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → QSORTH_IN_GA(X5, X7)
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
QSORTH_IN_GA(.(X1, X2)) → U11_GA(X1, X2, splitcD_in_ggaa(X2, X1))
U11_GA(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → QSORTH_IN_GA(X4)
U11_GA(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X5, qsortcH_in_ga(X4))
U13_GA(X1, X2, X5, qsortcH_out_ga(X4, X6)) → QSORTH_IN_GA(X5)
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3) → U41_ggaa(X1, X2, X3, lecC_in_gg(X1, X3))
splitcD_in_ggaa(.(X1, X2), X3) → U43_ggaa(X1, X2, X3, gtcE_in_gg(X1, X3))
qsortcH_in_ga([]) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2)) → U57_ga(X1, X2, splitcD_in_ggaa(X2, X1))
U41_ggaa(X1, X2, X3, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U43_ggaa(X1, X2, X3, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U57_ga(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X5, qsortcH_in_ga(X4))
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U58_ga(X1, X2, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X6, qsortcH_in_ga(X5))
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U59_ga(X1, X2, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, appendcI_in_ggga(X6, X1, X7))
U60_ga(X1, X2, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
appendcI_in_ggga([], X1, X2) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4) → U61_ggga(X1, X2, X3, X4, appendcI_in_ggga(X2, X3, X4))
U61_ggga(X1, X2, X3, X4, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
splitcD_in_ggaa(x0, x1)
qsortcH_in_ga(x0)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2)
lecC_in_gg(x0, x1)
U42_ggaa(x0, x1, x2, x3)
gtcE_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U58_ga(x0, x1, x2, x3)
U40_gg(x0, x1, x2)
U45_gg(x0, x1, x2)
U59_ga(x0, x1, x2, x3)
U60_ga(x0, x1, x2)
appendcI_in_ggga(x0, x1, x2)
U61_ggga(x0, x1, x2, x3, x4)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QSORTH_IN_GA(.(X1, X2)) → U11_GA(X1, X2, splitcD_in_ggaa(X2, X1))
POL(.(x1, x2)) = 1 + x2
POL(0) = 0
POL(QSORTH_IN_GA(x1)) = x1
POL(U11_GA(x1, x2, x3)) = x3
POL(U13_GA(x1, x2, x3, x4)) = x3
POL(U40_gg(x1, x2, x3)) = 0
POL(U41_ggaa(x1, x2, x3, x4)) = 1 + x2
POL(U42_ggaa(x1, x2, x3, x4)) = 1 + x4
POL(U43_ggaa(x1, x2, x3, x4)) = 1 + x2
POL(U44_ggaa(x1, x2, x3, x4)) = 1 + x4
POL(U45_gg(x1, x2, x3)) = 0
POL(U57_ga(x1, x2, x3)) = 0
POL(U58_ga(x1, x2, x3, x4)) = 0
POL(U59_ga(x1, x2, x3, x4)) = 0
POL(U60_ga(x1, x2, x3)) = 0
POL(U61_ggga(x1, x2, x3, x4, x5)) = 0
POL([]) = 0
POL(appendcI_in_ggga(x1, x2, x3)) = 0
POL(appendcI_out_ggga(x1, x2, x3, x4)) = 0
POL(gtcE_in_gg(x1, x2)) = 0
POL(gtcE_out_gg(x1, x2)) = 0
POL(lecC_in_gg(x1, x2)) = 0
POL(lecC_out_gg(x1, x2)) = 0
POL(qsortcH_in_ga(x1)) = 0
POL(qsortcH_out_ga(x1, x2)) = 0
POL(s(x1)) = 0
POL(splitcD_in_ggaa(x1, x2)) = x1
POL(splitcD_out_ggaa(x1, x2, x3, x4)) = x3 + x4
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3) → U41_ggaa(X1, X2, X3, lecC_in_gg(X1, X3))
splitcD_in_ggaa(.(X1, X2), X3) → U43_ggaa(X1, X2, X3, gtcE_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
U43_ggaa(X1, X2, X3, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U11_GA(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → QSORTH_IN_GA(X4)
U11_GA(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X5, qsortcH_in_ga(X4))
U13_GA(X1, X2, X5, qsortcH_out_ga(X4, X6)) → QSORTH_IN_GA(X5)
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3) → U41_ggaa(X1, X2, X3, lecC_in_gg(X1, X3))
splitcD_in_ggaa(.(X1, X2), X3) → U43_ggaa(X1, X2, X3, gtcE_in_gg(X1, X3))
qsortcH_in_ga([]) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2)) → U57_ga(X1, X2, splitcD_in_ggaa(X2, X1))
U41_ggaa(X1, X2, X3, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U43_ggaa(X1, X2, X3, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U57_ga(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X5, qsortcH_in_ga(X4))
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U58_ga(X1, X2, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X6, qsortcH_in_ga(X5))
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U59_ga(X1, X2, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, appendcI_in_ggga(X6, X1, X7))
U60_ga(X1, X2, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
appendcI_in_ggga([], X1, X2) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4) → U61_ggga(X1, X2, X3, X4, appendcI_in_ggga(X2, X3, X4))
U61_ggga(X1, X2, X3, X4, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
splitcD_in_ggaa(x0, x1)
qsortcH_in_ga(x0)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2)
lecC_in_gg(x0, x1)
U42_ggaa(x0, x1, x2, x3)
gtcE_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U58_ga(x0, x1, x2, x3)
U40_gg(x0, x1, x2)
U45_gg(x0, x1, x2)
U59_ga(x0, x1, x2, x3)
U60_ga(x0, x1, x2)
appendcI_in_ggga(x0, x1, x2)
U61_ggga(x0, x1, x2, x3, x4)
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
qsortcA_in_a([]) → qsortcA_out_a([])
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
qsortcF_in_ga([], []) → qsortcF_out_ga([], [])
qsortcF_in_ga(.(X1, []), X2) → U46_ga(X1, X2, qsortcA_in_a(X3))
U46_ga(X1, X2, qsortcA_out_a(X3)) → U47_ga(X1, X2, X3, qsortcA_in_a(X4))
U47_ga(X1, X2, X3, qsortcA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qsortcF_out_ga(.(X1, []), X2)
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
APPENDB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
APPENDB_IN_GGGA(.(X1, X2), X3, X4) → APPENDB_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U25_GA(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSORTF_IN_GA(.(X2, X5), X7)
qsortcA_in_a([]) → qsortcA_out_a([])
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
qsortcH_in_ga([], []) → qsortcH_out_ga([], [])
qsortcH_in_ga(.(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qsortcH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qsortcH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qsortcH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qsortcH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, .(X1, X2)) → appendcI_out_ggga([], X1, X2, .(X1, X2))
appendcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qsortcH_out_ga(.(X1, X2), X3)
qsortcF_in_ga([], []) → qsortcF_out_ga([], [])
qsortcF_in_ga(.(X1, []), X2) → U46_ga(X1, X2, qsortcA_in_a(X3))
U46_ga(X1, X2, qsortcA_out_a(X3)) → U47_ga(X1, X2, X3, qsortcA_in_a(X4))
U47_ga(X1, X2, X3, qsortcA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, .(X1, X2)) → appendcB_out_ggga([], X1, X2, .(X1, X2))
appendcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qsortcF_out_ga(.(X1, []), X2)
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qsortcF_in_ga(.(X2, X5), X7))
qsortcF_in_ga(.(X1, .(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, gtcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, gtcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qsortcH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qsortcH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qsortcH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qsortcH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qsortcF_out_ga(.(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qsortcF_out_ga(.(X1, .(X2, X3)), X4)
QSORTF_IN_GA(.(X1, .(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, lecC_in_gg(X2, X1))
U25_GA(X1, X2, X3, X4, lecC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSORTF_IN_GA(.(X2, X5), X7)
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3, .(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
splitcD_in_ggaa(.(X1, X2), X3, X4, .(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U41_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U43_ggaa(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
QSORTF_IN_GA(.(X1, .(X2, X3))) → U25_GA(X1, X2, X3, lecC_in_gg(X2, X1))
U25_GA(X1, X2, X3, lecC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, splitcD_in_ggaa(X3, X1))
U27_GA(X1, X2, X3, splitcD_out_ggaa(X3, X1, X5, X6)) → QSORTF_IN_GA(.(X2, X5))
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3) → U41_ggaa(X1, X2, X3, lecC_in_gg(X1, X3))
splitcD_in_ggaa(.(X1, X2), X3) → U43_ggaa(X1, X2, X3, gtcE_in_gg(X1, X3))
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U41_ggaa(X1, X2, X3, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U43_ggaa(X1, X2, X3, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
lecC_in_gg(x0, x1)
splitcD_in_ggaa(x0, x1)
U40_gg(x0, x1, x2)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
gtcE_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U45_gg(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QSORTF_IN_GA(.(X1, .(X2, X3))) → U25_GA(X1, X2, X3, lecC_in_gg(X2, X1))
POL(.(x1, x2)) = 1 + x2
POL(0) = 0
POL(QSORTF_IN_GA(x1)) = x1
POL(U25_GA(x1, x2, x3, x4)) = 1 + x3
POL(U27_GA(x1, x2, x3, x4)) = 1 + x4
POL(U40_gg(x1, x2, x3)) = 0
POL(U41_ggaa(x1, x2, x3, x4)) = 1 + x2
POL(U42_ggaa(x1, x2, x3, x4)) = 1 + x4
POL(U43_ggaa(x1, x2, x3, x4)) = 1 + x2
POL(U44_ggaa(x1, x2, x3, x4)) = x4
POL(U45_gg(x1, x2, x3)) = 0
POL([]) = 0
POL(gtcE_in_gg(x1, x2)) = 0
POL(gtcE_out_gg(x1, x2)) = 0
POL(lecC_in_gg(x1, x2)) = 0
POL(lecC_out_gg(x1, x2)) = 0
POL(s(x1)) = 0
POL(splitcD_in_ggaa(x1, x2)) = x1
POL(splitcD_out_ggaa(x1, x2, x3, x4)) = x3
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3) → U41_ggaa(X1, X2, X3, lecC_in_gg(X1, X3))
splitcD_in_ggaa(.(X1, X2), X3) → U43_ggaa(X1, X2, X3, gtcE_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
U43_ggaa(X1, X2, X3, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U25_GA(X1, X2, X3, lecC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, splitcD_in_ggaa(X3, X1))
U27_GA(X1, X2, X3, splitcD_out_ggaa(X3, X1, X5, X6)) → QSORTF_IN_GA(.(X2, X5))
lecC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(.(X1, X2), X3) → U41_ggaa(X1, X2, X3, lecC_in_gg(X1, X3))
splitcD_in_ggaa(.(X1, X2), X3) → U43_ggaa(X1, X2, X3, gtcE_in_gg(X1, X3))
U40_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U41_ggaa(X1, X2, X3, lecC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U43_ggaa(X1, X2, X3, gtcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, .(X1, X4), X5)
gtcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(.(X1, X2), X3, X4, .(X1, X5))
U45_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
lecC_in_gg(x0, x1)
splitcD_in_ggaa(x0, x1)
U40_gg(x0, x1, x2)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
gtcE_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U45_gg(x0, x1, x2)